Inference at * 2 1 
Iof proof for Lemma decidable-filter:

.....wf..... NILNIL

1. T : Type
2. T List
3. u : T
4. v : T List
5. P:({x:T| (x  v)} ).
5. (xv. Dec(P(x)))  (L':T List. (L'  v & (x:T. (x  L')  ((x  v) & P(x)))))
6. P : {x:T| (x  [u / v])} 
7. x[u / v]. Dec(P(x))
  P  {x:T| (x  v)}  

latex

 by ((ExtWith [`z'] [{x:T| (x  [u / v])} ]) 
CollapseTHEN (MaAuto)) 

latex

C.

Definitions	x:AB(x), {x:A| B(x)} , (x  l), [car / cdr], , A c B, S  T, |g|, , A, False, Void, ||as||, A  B, , #$n, a < b, l[i], last(L), [], {T}, , P & Q, f(a), Dec(P), P  Q, left + right, L1  L2, P  Q, increasing(f;k), x(s), P  Q, P  Q, x:A. B(x), x:A  B(x), xL. P(x), type List, x:A. B(x), Type, s = t, t  T
Lemmas	member wf, subtype rel wf, nat wf, length wf1, select wf, cons member, l member wf